1  t0<t  (1)

2  isconst(e)  (2)

3  isconst(e)⊃compile(e,t)=mkli(val(e))  

4  compile(e,t)=mkli(val(e))  (2)

5  outcome(compile(e,t),load(xi))=outcome(compile(e,t),load(xi))  

6  outcome(compile(e,t),load(xi))=outcome(mkli(val(e)),load(xi))  (2)

7  isli(mkli(val(e)))⊃outcome(mkli(val(e)),load(xi))=a(ac,arg(mkli(val(e))),load(xi))  

8  isli(mkli(val(e)))  

9  outcome(mkli(val(e)),load(xi))=a(ac,arg(mkli(val(e))),load(xi))  

10  val(e)=arg(mkli(val(e)))  

11  outcome(mkli(val(e)),load(xi))=a(ac,val(e),load(xi))  

12  isconst(e)⊃value(e,xi)=val(e)  

13  value(e,xi)=val(e)  (2)

14  outcome(mkli(val(e)),load(xi))=a(ac,value(e,xi),load(xi))  (2)

15  outcome(compile(e,t),load(xi))=a(ac,value(e,xi),load(xi))  (2)

16  equiv(a(ac,value(e,xi),load(xi)),a(ac,value(e,xi),load(xi)),t)  

17  equiv(outcome(compile(e,t),load(xi)),a(ac,value(e,xi),load(xi)),t)  (2)

18  isconst(e)⊃equiv(outcome(compile(e,t),load(xi)),a(ac,value(e,xi),load(xi)),t)  

19  isvar(e)  (19)

20  isvar(e)⊃compile(e,t)=mkload(map(e))  

21  compile(e,t)=mkload(map(e))  (19)

22  isload(mkload(map(e)))⊃outcome(mkload(map(e)),load(xi))=a(ac,cc(arg(mkload(map(e))),load(xi)),load(xi))  

23  isload(mkload(map(e)))  

24  outcome(mkload(map(e)),load(xi))=a(ac,cc(arg(mkload(map(e))),load(xi)),load(xi))  

25  outcome(compile(e,t),load(xi))=a(ac,cc(arg(mkload(map(e))),load(xi)),load(xi))  (19)

26  map(e)=arg(mkload(map(e)))  

27  outcome(compile(e,t),load(xi))=a(ac,cc(map(e),load(xi)),load(xi))  (19)

28  isvar(e)⊃cc(map(e),load(xi))=c(e,xi)  

29  cc(map(e),load(xi))=c(e,xi)  (19)

30  outcome(compile(e,t),load(xi))=a(ac,c(e,xi),load(xi))  (19)

31  isvar(e)⊃value(e,xi)=c(e,xi)  

32  value(e,xi)=c(e,xi)  (19)

33  outcome(compile(e,t),load(xi))=a(ac,value(e,xi),load(xi))  (19)

34  equiv(a(ac,value(e,xi),load(xi)),a(ac,value(e,xi),load(xi)),t)  

35  equiv(outcome(compile(e,t),load(xi)),a(ac,value(e,xi),load(xi)),t)  (19)

36  isvar(e)⊃equiv(outcome(compile(e,t),load(xi)),a(ac,value(e,xi),load(xi)),t)